(set-logic UFNIA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(assert (forall ((q0 Int) (q1 Bool) (q2 Bool) (q3 Int)) (not (> q0 q3))))
(declare-const v8 Bool)
(declare-const i2 Int)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i3 Int)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const i4 Int)
(declare-const v14 Bool)
(assert (forall ((q4 Int)) v5))
(push 1)
(pop 1)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert (forall ((q5 Int) (q6 Int) (q7 Int)) (not (> q7 q7))))
(declare-const v20 Bool)
(push 1)
(declare-const v21 Bool)
(declare-sort S0 0)
(declare-const v22 Bool)
(push 1)
(declare-const S0-0 S0)
(pop 1)
(declare-sort S1 0)
(declare-const v23 Bool)
(assert (exists ((q8 Int) (q9 Int)) v8))
(pop 1)
(declare-const i5 Int)
(declare-const v24 Bool)
(assert (or v7 v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1))
(assert (or v1 v10 (or v16 (distinct 187 187) (>= 187 73))))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) v7 v7))
(assert (or (distinct 187 187) (or v16 (distinct 187 187) (>= 187 73)) v9))
(assert (or (distinct 187 187) (>= 187 73) v1))
(assert (or v10 v1 v10))
(assert (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))))
(assert (or v7 (distinct 187 187) (>= 187 73)))
(assert (or v13 (distinct 187 187) (>= 187 73)))
(assert (or v1 v13 v10))
(assert (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v7))
(assert (or (>= 187 73) (>= 79 642) (>= 187 73)))
(assert (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))))
(assert (or (>= 187 73) v13 v1))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (or v13 (>= 187 73) v1))
(assert (or v7 v13 v9))
(assert (or (>= 79 642) (>= 187 73) v13))
(assert (or v13 v7 (>= 187 73)))
(assert (or v13 v13 (>= 79 642)))
(assert (or v1 (or v16 (distinct 187 187) (>= 187 73)) (or v16 (distinct 187 187) (>= 187 73))))
(assert (or v13 v1 (>= 187 73)))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13))
(assert (or v7 v9 v9))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (or v13 (>= 79 642) (distinct 187 187)))
(assert (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)))
(assert (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187)))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9 v1))
(assert (or (distinct 187 187) v7 (distinct 187 187)))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (or (>= 187 73) v1 (>= 187 73)))
(assert (or v1 v1 v13))
(assert (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))))
(assert (or (>= 79 642) v9 (>= 79 642)))
(assert (or v10 v7 (>= 79 642)))
(assert (or v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73)))
(assert (or v1 (>= 187 73) v13))
(assert (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9))
(assert (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10))
(assert (or v9 v7 (>= 79 642)))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v7))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642)))
(assert (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10))
(assert (or v1 v9 v10))
(assert (or v13 v13 v7))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) v1))
(assert (or (distinct 187 187) (>= 79 642) (>= 79 642)))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73) (or v16 (distinct 187 187) (>= 187 73))))
(assert (or v7 v7 v1))
(assert (or (>= 79 642) v9 (>= 187 73)))
(assert (or (>= 187 73) (or v16 (distinct 187 187) (>= 187 73)) v1))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1))
(assert (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (or (distinct 187 187) v10 v9))
(assert (or (>= 187 73) (or v16 (distinct 187 187) (>= 187 73)) v10))
(assert (or (distinct 187 187) v10 v1))
(assert (or (>= 187 73) v13 v1))
(assert (and (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v7 v13 v9)))
(assert (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))))
(assert (or (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9)))
(assert (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v7 (distinct 187 187)) (or (or v16 (distinct 187 187) (>= 187 73)) v7 v7)))
(assert (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (and (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v1 v13 v10) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or v1 (or v16 (distinct 187 187) (>= 187 73)) (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) (>= 187 73) v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))))
(check-sat)
(assert (or v7 v9 v9))
(assert (=> (or (distinct 187 187) (>= 187 73) v1) (or v1 v9 v10)))
(assert (or (and (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v7 v13 v9)) (or (distinct 187 187) v10 v9)))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) v1))
(assert (=> (or (distinct 187 187) (>= 79 642) (>= 79 642)) (or v13 v13 v7)))
(assert (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))))
(check-sat)
(assert (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10))
(assert (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 (>= 79 642) (distinct 187 187)) (or (>= 79 642) v9 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)))
(assert (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v7 v9 v9) (or (>= 79 642) v9 (>= 187 73)) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 (>= 79 642) (distinct 187 187)) (or (>= 79 642) v9 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1))))
(assert (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)))
(assert (=> (or (distinct 187 187) v10 v9) (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))))
(assert (or (or v1 v1 v13) (or (distinct 187 187) (>= 79 642) (>= 79 642))))
(assert (and (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v7 v9 v9) (or (>= 79 642) v9 (>= 187 73)) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 (>= 79 642) (distinct 187 187)) (or (>= 79 642) v9 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1))) (or (>= 187 73) v13 v1)))
(assert (and (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 v1 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73) (or v16 (distinct 187 187) (>= 187 73))) (or (>= 79 642) v9 (>= 187 73)) (or v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73))))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642)))
(assert (=> (or (>= 79 642) v9 (>= 187 73)) (or v9 v7 (>= 79 642))))
(assert (or (or (>= 79 642) v9 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))))
(assert (and (or (>= 79 642) v9 (>= 187 73)) (and (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v7 (distinct 187 187) (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v7) (or v13 v13 v7) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v1 (>= 187 73) v13) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))))
(assert (and (or v13 v1 (>= 187 73)) (or (>= 187 73) v1 (>= 187 73)) (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (or v13 (>= 79 642) (distinct 187 187)) (or (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9) (or (or v1 v1 v13) (or (distinct 187 187) (>= 79 642) (>= 79 642)))))
(assert (and (and (or (>= 187 73) (or v16 (distinct 187 187) (>= 187 73)) v10) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9) (or (distinct 187 187) (or v16 (distinct 187 187) (>= 187 73)) v9) (or v13 v13 v7) (and (or (distinct 187 187) v10 v9) (and (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v7 (distinct 187 187) (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v7) (or v13 v13 v7) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v1 (>= 187 73) v13) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)) (or (distinct 187 187) (>= 79 642) (>= 79 642)) (=> (or (distinct 187 187) (>= 79 642) (>= 79 642)) (or v13 v13 v7)) (or (>= 187 73) v1 (>= 187 73)) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187))) (or (or v1 v1 v13) (or (distinct 187 187) (>= 79 642) (>= 79 642))) (and (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 v1 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73) (or v16 (distinct 187 187) (>= 187 73))) (or (>= 79 642) v9 (>= 187 73)) (or v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73))) (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v10 v1 v10)) (and (or v13 v1 (>= 187 73)) (or (>= 187 73) v1 (>= 187 73)) (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (or v13 (>= 79 642) (distinct 187 187)) (or (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9) (or (or v1 v1 v13) (or (distinct 187 187) (>= 79 642) (>= 79 642)))) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187)) (or v7 (distinct 187 187) (>= 187 73)) (or (distinct 187 187) v10 v1) (or v13 v13 v7) (and (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v1 v13 v10) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or v1 (or v16 (distinct 187 187) (>= 187 73)) (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) (>= 187 73) v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (or v1 v9 v10)))
(assert (=> (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (distinct 187 187) v7 (distinct 187 187))))
(assert (or (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v7 v9 v9) (or (>= 79 642) v9 (>= 187 73)) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 (>= 79 642) (distinct 187 187)) (or (>= 79 642) v9 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)))))
(assert (and (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (and (or (distinct 187 187) v10 v9) (and (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v7 (distinct 187 187) (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v7) (or v13 v13 v7) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v1 (>= 187 73) v13) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)) (or (distinct 187 187) (>= 79 642) (>= 79 642)) (=> (or (distinct 187 187) (>= 79 642) (>= 79 642)) (or v13 v13 v7)) (or (>= 187 73) v1 (>= 187 73)) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187))) (or (distinct 187 187) v10 v1) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (=> (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (distinct 187 187) v7 (distinct 187 187)))))
(assert (=> (or (distinct 187 187) (>= 187 73) v1) (or v1 v9 v10)))
(assert (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9 v1))
(assert (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))
(assert (and (and (or (>= 187 73) (or v16 (distinct 187 187) (>= 187 73)) v10) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9) (or (distinct 187 187) (or v16 (distinct 187 187) (>= 187 73)) v9) (or v13 v13 v7) (and (or (distinct 187 187) v10 v9) (and (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v7 (distinct 187 187) (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v7) (or v13 v13 v7) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v1 (>= 187 73) v13) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)) (or (distinct 187 187) (>= 79 642) (>= 79 642)) (=> (or (distinct 187 187) (>= 79 642) (>= 79 642)) (or v13 v13 v7)) (or (>= 187 73) v1 (>= 187 73)) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187))) (or (or v1 v1 v13) (or (distinct 187 187) (>= 79 642) (>= 79 642))) (and (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 v1 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73) (or v16 (distinct 187 187) (>= 187 73))) (or (>= 79 642) v9 (>= 187 73)) (or v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 187 73))) (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v10 v1 v10)) (and (or v13 v1 (>= 187 73)) (or (>= 187 73) v1 (>= 187 73)) (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (or v13 (>= 79 642) (distinct 187 187)) (or (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v9) (or (or v1 v1 v13) (or (distinct 187 187) (>= 79 642) (>= 79 642)))) (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187)) (or v7 (distinct 187 187) (>= 187 73)) (or (distinct 187 187) v10 v1) (or v13 v13 v7) (and (or (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (distinct 187 187)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v1 v13 v10) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (or v16 (distinct 187 187) (>= 187 73)) v9 v1) (or v1 (or v16 (distinct 187 187) (>= 187 73)) (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) (>= 187 73) v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (or v1 v9 v10)))
(assert (and (and (or v1 v13 v10) (and (or (>= 79 642) v9 (>= 187 73)) (and (or v10 (or v16 (distinct 187 187) (>= 187 73)) (>= 187 73)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v7 (distinct 187 187) (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v7) (or v13 v13 v7) (or (or v13 v7 (>= 187 73)) (=> (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or v1 (>= 187 73) v13) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)) (or v9 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)))) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v10) (or v13 (distinct 187 187) (>= 187 73)) (or (distinct 187 187) v10 v1) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642)) (or v7 v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v1 v1 v13) (or (distinct 187 187) (or v16 (distinct 187 187) (>= 187 73)) v9) (or (distinct 187 187) (>= 79 642) (>= 79 642))) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1) (or (>= 79 642) v9 (>= 187 73)) (or v13 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v7) (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v7 (distinct 187 187)) (or (or v16 (distinct 187 187) (>= 187 73)) v7 v7)) (or v7 v9 v9)))
(assert (or (and (or (distinct 187 187) v7 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v10 (or v16 (distinct 187 187) (>= 187 73))) (or v7 v13 v9) (or (>= 187 73) v1 (>= 187 73)) (or v9 (>= 187 73) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (>= 79 642) v10 (or v16 (distinct 187 187) (>= 187 73))) (or (distinct 187 187) v10 v9) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v13) (or (>= 187 73) (distinct 187 187) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15))) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) v1 (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v7 v9 v9) (or (>= 79 642) v9 (>= 187 73)) (and (or (or v16 (distinct 187 187) (>= 187 73)) (>= 79 642) (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15)) (or v13 (>= 79 642) (distinct 187 187)) (or (>= 79 642) v9 (>= 187 73)) (or (and (<= 79 867) v3 (> i3 i3) v6 v0 v20 v15) (>= 79 642) v1)))))
(check-sat)
(exit)
